$\forall$$A$:Type, $f$:$a$:$A$ fp$\rightarrow$ Type, ${\it eq}$:EqDecider($A$), $x$:$A$, $z$:Type. $f$($x$)?$z$ $\in$ Type